package kodkod.analysis;

import java.io.PrintWriter;
import java.util.ArrayList;

import kodkod.analysis.visitor.*;
import kodkod.ast.Formula;
import kodkod.ast.LeafExpression;
import kodkod.ast.Relation;
import kodkod.engine.fol2sat.Translation;

public class AnalyzeRelations {
	
	MinimumDistance minDist;
	IncomingEdges inEdges;
	IncomingPaths inPaths;
	QuantifierType qType;
	
	Translation translation;
	
	public AnalyzeRelations(Formula formula, Translation translation) {
		this.translation = translation;
		
		minDist = new MinimumDistance(formula);
		inEdges = new IncomingEdges(formula);
		inPaths = new IncomingPaths(formula);
		qType = new QuantifierType(formula);
	}
	
	public void printAnalyticInfo(PrintWriter out) {
		Object[] relations = translation.getPrimaryVarUsage().keySet().toArray();
		
		out.println();
		out.println("Number of Relations: " + relations.length);
		out.println();
		
		for (int i = 0; i < relations.length; i++) {
			Relation relation = (Relation)relations[i];
			LeafExpression leaf = (LeafExpression)relations[i];
			out.print("Relation " + i + ": " + relation.name());
			out.print(", nofVars: " + translation.getPrimaryVarUsage().get(relation).size());
			out.print(", nofEdges: " + inEdges.counter.get(leaf));
			out.print(", nofPaths: " + inPaths.counter.get(leaf));
			out.print(", distanceToRoot: " + minDist.distance.get(leaf));
			if (qType.allQuantified.contains(leaf)) {
				out.println(", ALL quantified");
			}
			if (qType.existQuantified.contains(leaf)) {
				out.println(", EXIST quantified");
			}
			out.println();
		}
	}
}
